COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00014 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "↓"
.FONT B "GRFX35";
.FONT C "GRK30";
.AT "!r" ⊂"%Cαr%*"⊃
.AT "!8" ⊂"%2α~%*"⊃
.turn on "→"
.cb Stanford Artificial Intelligence Project

.begin nofill

Memo 1→March 22, 1963
.end
.cb PREDICATE CALCULUS WITH "UNDEFINED" AS A TRUTH VALUE
.skip 1
.once center
by John McCarthy

	We would like to use predicate calculus in the mathematical theory of
computation.  In particular, we would like to write formulas involving
recursively defined predicates and functions.  The trouble is that
recursively defined predicates are not guaranteed to be defined for all
values of their arguments, and therefore, it is not clear how to interpret
formulas involving them.

	We shall give an interpretation of predicate calculus formulas
involving partial predicates and extend the notions of truth, valid
formula and tautology.  We have three truth values, ⊗t for ⊗true, ⊗f for
⊗false, and ⊗u for ⊗undefined.  The well-formed formulas are the same as
in predicate calculus except that we have a new propositional operator
* defined by
.skip
.begin narrow 8; nofill
*%2t = t
*%2f = t
*%2u = f
.end

We shall call our system EFC.

The truth of a formula is determined from its constituents as follows:

1. An elementary form ⊗p(x,...,z) is ⊗true, ⊗false, or ⊗undefined for each
set of values of ⊗x,...,z. 

2. The truth values of propositional combinations is determined by the
truth-tables.
.skip
.begin nofill; preface 0 mills
.select B
.turn on "∂∞"
.turn on "@" for "\"
.tabs 14,20,26,32,38
.at "|" ⊂"α~"⊃
∂(11)%2π%B@|∂(16)%2¬π%B@|∂(22)%2*%2π%B
∂(10)∞α@β∞α@β∞α@
∂(11)t@|∂(17)f@|∂(23)t
∂(11)f@|∂(17)t@|∂(23)t
∂(11)u@|∂(17)u@|∂(23)f
.skip 2
∂(10)%2π!r%B@|∂(16)%2π∧!r%B@|∂(22)%2π∨!r%B@|∂(28)%2π⊃!r%B@|∂(34)%2π≡!r%B
∂(10)∞α@β∞α@β∞α@β∞α@β∞α@
∂(10)tt@|∂(17)t@|∂(23)t@|∂(29)t@|∂(35)t
∂(10)tf@|∂(17)f@|∂(23)t@|∂(29)f@|∂(35)f
∂(10)tu@|∂(17)u@|∂(23)t@|∂(29)u@|∂(35)u
∂(10)ft@|∂(17)f@|∂(23)t@|∂(29)t@|∂(35)f
∂(10)ff@|∂(17)f@|∂(23)f@|∂(29)t@|∂(35)t
∂(10)fu@|∂(17)f@|∂(23)u@|∂(29)t@|∂(35)u
∂(10)ut@|∂(17)u@|∂(23)u@|∂(29)u@|∂(35)u
∂(10)uf@|∂(17)u@|∂(23)u@|∂(29)u@|∂(35)u
∂(10)uu@|∂(17)u@|∂(23)u@|∂(29)u@|∂(35)u
.end

The truth values of the last two are in accordance with the definitions
.skip
.begin narrow 8; nofill
%2π ⊃ !r = ¬π ∨ !r
π ≡ !r = (π ⊃ !r) ∧ (!r ⊃ π)
.end

%1where ⊗= is used in its ordinary sense as a metamathematical symbol.
They are the same as the conditional expression definitions of [1].  As
explained in that paper the noncommutativity of %2π∧!r %1and %2π∨!r %1arises
from the convention that ⊗π is evaluated first, so that if ⊗π is false, !r need
not be evaluated to get %2π∧!r.%1 

3. %2∀x. π(x) %1is true if ⊗π(x) is true for all x, undefined if ⊗π(x) is
undefined for some ⊗x and false otherwise.

4. %2∃x. π(x) %1is true if ⊗π(x) is true for some ⊗x and is defined for all
⊗x, undefined if ⊗π(x) is undefined for some ⊗x, and false otherwise.

	If we consider formulas with no quantifiers we get an extended propositional
calculus EPC.  A formula is called a tautology if it is true for all values of
its arguments.  Ordinary tautologies are not tautologies of EPC since they
are undefined if all the propositional variables are undefined.  However,
if ⊗π is an ordinary tautology, then *%2π ⊃ π %1is a tautology of EPC so
that formulas like

.once indent 8
*%2(p⊃(q⊃p)) ⊃ (p⊃(q⊃p))

%1are tautologies.  Whether a formula is a tautology can be determined by
truth tables.

The equivalence of two formulas ⊗π and !r is not expressed by %2π ≡ !r %1being a 
tautology, e.g. %2!r ≡ !r %1is not a tautology.  Therefore, we define

.once indent 8
%2π !8 !r = (*%2π ≡ *%2!r) ∧ α[*%2π ⊃ (π ≡ !r)α],

%1and %2π !8 !r %1 does express the equivalence of ⊗π and !r.  This is the
strong equivalence of [1].  The weak equivalence of that paper is written

.once indent 8
%2π !8↓w !r = *π ∧ *!r ⊃ (π ≡ !r)

%1where ⊗π and !r do not involve *.

The following formulas are all tautologies
.skip
.begin narrow 8; nofill
%2*(p ∧ q) !8 *p ∧ (p ⊃ *q)
%2*(p ∨ q) !8 *p ∧ (¬p ⊃ *q)
%2*(p ≡ q) !8 *p ∧ *q
%2*¬p !8 *p
%2**p
%2*(p !8 q)
.end

%1The valid formulas of EFC in a domain are those which are true for all
assignments of partial predicates to the predicate letters.  Many questions
about proof procedures for EFC are answered by a construction which gives
for every formula ⊗π of EFC a formula %2π↓1 %1of FC (the usual predicate
calculus) such that ⊗π is valid in the domain if and only if %2π↓1 %1is valid.
Actually, we shall construct three formulas %2π↓1, π↓2 qand π↓3 %1of FC
which are true when ⊗π is true, false, or undefined respectively.  The
construction is given by the following table.
.skip
.begin nofill; preface 0 mills; group
.select B
.turn on "∂∞"
.turn on "@" for "\"
.tabs 20,36,52,65
.at "|" ⊂"α~"⊃
.at "↓1" ⊂"%41%*"⊃
.at "↓2" ⊂"%42%*"⊃
.at "↓3" ⊂"%43%*"⊃
∂(15)%2π%B@|∂(28)%2π↓1%B@|∂(44)%2π↓2%B@|∂(57)%2π↓3%B
∂(10)∞α@β∞α@β∞α@∞α@
∂(10)%2p(x,...,z)%B@|∂(22)%2p↓1(x,...,z)%B@|∂(38)%2p↓2(x,...,z)%B@|∂(54)%2p↓3(x,...,z)
∂(10)%2¬π%B@|∂(22)%2π↓2%B@|∂(38)%2π↓1%B@|∂(54)%2π↓3
∂(10)%2*π%B@|∂(22)%2π↓1∨π↓2%B@|∂(38)%2π↓3%B@|∂(54)%2f
∂(10)%2π∧!r%B@|∂(22)%2π↓1∧!r↓1%B@|∂(38)%2π↓2∨(π↓1!r↓2)%B@|∂(54)%2π↓3∨(π↓1∧!r↓3)
∂(10)%2π∨!r%B@|∂(22)%2π↓1∨(π↓2∧!r↓1)%B@|∂(38)%2π↓2∧!r↓2%B@|∂(54)%2π↓3∨(π↓2∧!r↓3)
∂(10)%2π⊃!r%B@|∂(22)%2π↓2∨(π↓1∧!r↓1)%B@|∂(38)%2π↓1∧!r↓2%B@|∂(54)%2π↓3∨(π↓1∧!r↓3)
∂(10)%2π≡!r%B@|∂(22)%2(π↓1∧!r↓1)∨(π↓2∧!r↓2))%B@|∂(38)%2(π↓1∧!r↓2)∨(π↓2∧!r↓1)%B@|∂(54)%2π↓3∨!r↓3
∂(10)%2∀x.π%B@|∂(22)%2∀x.π↓1%B@|∂(38)%2(∃x.π↓2)∧(∀x.¬π↓3)%B@|∂(54)%2∃x.π↓3
∂(10)%2∃x.π%B@|∂(22)%2(∃x.π↓1)∧(∀x.¬π↓3)%B@|∂(38)%2(∀x.π↓2)%B@|∂(54)%2∃x.π↓3
.end

That %2π↓1, π↓2 %1and %2π↓3 %1have the required properties is obvious from the
construction.  This result shows that EFC is semi-decidable so that it should
be possible to obtain a complete set of axioms and rules of inference.  The
method of semantic tableaux can be applied directly to EFC, but, at least
in its most obvious form, it is impractical for all but the simplest examples
because the number of cases that has to be considered increases rapidly.

The choice of definitions for the quantifiers requires some explanation.
Our choice has the disadvantage that one cannot prove %2∃x.π(x) %1simply by
exhibiting an a such that %2π(a) %1since if some %2π(b) %1is undefined
%2∃x.π(x) %1is considered undefined.  However, the other possible
quantifiers are definable in terms of ours.  For example, we can define

.once indent 8
%2(∃'x).π(x) = ∃x.*π(x)∧π(x)

%1which has the above mentioned property.

Note of February 8, 1979.  This AI Memo 1 of March 22, 1963 is reprinted
with only trivial notational changes.  The reference, which was omitted
from the original, is to 
%3McCarthy, John%1 (1963) "A Basis for a Mathematical Theory of Computation", in
P. Braffort and D. Hirschberg (eds.), %2Computer Programming and Formal Systems%1,
pp. 33-70.  North-Holland Publishing Company, Amsterdam.